VERS5 
NIL 
((EPSILONDEF SETS#4) (SET_EXTENSIONALITY SETS#5) (CHOICE SETS#9) (DEMORGAN NORMAL#5) (DEMORGAN1 NORMAL#6) (EXCLUDED_MIDDLE NORMAL#7) (TRANS_COND NORMAL#8) (DISJUNCT_SUBST NORMAL#9) (INCONSISTENT NORMAL#10) (ZERO_NOT_SUCCESSOR NATNUM#6) (SUCCESSOREQ NATNUM#7) (PROOF_BY_INDUCTION NATNUM#8) (LANDAU_TH1 NATNUM#9) (LANDAU_TH2 NATNUM#10) (LANDAU_TH3 NATNUM#11) (LANDAU_TH4 NATNUM#15) (COMMUTADD NATNUM#17) (LANDAU_TH7 NATNUM#18) (LANDAU_TH8 NATNUM#19) (TRCT0 NATNUM#20) (TRCT1 NATNUM#21) (TRCT2 NATNUM#22) (TRCT3 NATNUM#23) (PLUSDEF1 NATNUM#24) (LPLUSCAN NATNUM#26) (RPLUSCAN NATNUM#27) (ADDTOZERO NATNUM#28) (LANDAU_DEF2 ORDERING#3) (TOTALORD ORDERING#5) (STRICT1 ORDERING#6) (STRICT2 ORDERING#7) (STRICT3 ORDERING#8) (GREATERP_LESSP ORDERING#9) (GRTEQP_LSSEQP ORDERING#14) (TRANSITIVITY_OF_ORDER ORDERING#15) (TRANSITIVITY_OF_GREATERP ORDERING#16) (LSSEQP_LESSP_LESSP ORDERING#17) (LESSP_LSSEQP_LESSP ORDERING#18) (TRANSITIVITY_OF_LSSEQP ORDERING#19) (INCREASING ORDERING#20) (SUCCESSORLESS ORDERING#21) (RPLUS_GREATCAN ORDERING#22) (RPLUS_LESSCAN ORDERING#23) (LANDAU_TH21 ORDERING#24) (LANDAU_A_TH22 ORDERING#25) (LANDAU_B_TH22 ORDERING#26) (LANDAU_TH23 ORDERING#27) (LANDAU_A_TH24 ORDERING#28) (ZEROLEAST1 ORDERING#29) (ZEROLEAST2 ORDERING#30) (LANDAU_B_TH24 ORDERING#31) (LANDAU_TH25 ORDERING#32) (LANDAU_TH26 ORDERING#33) (LANDAU_TH27 ORDERING#34) (LANDAU_DEF6 MULTIP#2) (TIMSUCC MULTIP#5) (LTIMESCAN MULTIP#6) (RTIMESCAN MULTIP#7) (COMMUTMULT MULTIP#8) (LTIMESTOZERO MULTIP#9) (RTIMESTOZERO MULTIP#10) (NOZERODIVISORS MULTIP#11) (TIMESFACT MULTIP#11) (LDISTRIB MULTIP#12) (RDISTRIB MULTIP#13) (LANDAU_A_TH32 MULTIP#14) (LANDAU_D_TH32 MULTIP#15) (LANDAU_A_TH33 MULTIP#16) (LANDAU_B_TH33 MULTIP#17) (LANDAU_C_TH33 MULTIP#18) (LANDAU_TH34 MULTIP#19) (LANDAU_A_TH35 MULTIP#20) (LANDAU_B_TH35 MULTIP#21) (LANDAU_TH36 MULTIP#22) (ALLDEF ALL#3) (SOMEDEF ALL#4) (ALLFACT ALL#5) (SOMEFACT ALL#6) (NORMAL NORMAL#1 NORMAL#2 NORMAL#3 NORMAL#4) (TRICOTOMY NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23) (SUCCFACTS NATNUM#6 NATNUM#7 ORDERING#21 ORDERING#29 ORDERING#30) (TIMESFACTS MULTIP#2 MULTIP#4 MULTIP#5 MULTIP#6 MULTIP#7 MULTIP#8 MULTIP#9 MULTIP#10 MULTIP#12 MULTIP#13) (PLUSFACTS NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#22 ORDERING#23 MULTIP#12 MULTIP#13) (SIMPINFO NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4)) (NIL . (DECL (ARB ARB1 ARB2) (TYPE: (TY& . ?ARBITRARY))) . ((ARB2 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (ARB1 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (ARB . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 1 .)(NIL . (DECL (SETVAR SETVAR1) (TYPE: (TY& . |(?ARBITRARY)→TRUTHVAL|))) . ((SETVAR1 . (|(?ARBITRARY)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#2 . NIL . VARIABLE .)) (SETVAR . (|(?ARBITRARY)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 2 .)(|∀P P1 P2.(P∨P1)∧P2≡P∧P2∨P1∧P2| . (AXIOM (TM& . |∀P P1 P2.(P∨P1)∧P2≡P∧P2∨P1∧P2|)) . ((P2 . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .)) (P1 . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .)) (P . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .))) . NIL . (NORMAL#1) . NIL . NORMAL . NIL . 1 .)(NIL . (DECL (I J K N M) (SORT: (TM& . NATNUM)) (TYPE: (TY& . GROUND))) . ((M . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .)) (N . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .)) (K . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .)) (J . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .)) (I . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 1 .)(NIL . (DECL (A B C SET) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((SET . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#2 . NIL . VARIABLE .)) (C . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#2 . NIL . VARIABLE .)) (B . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#2 . NIL . VARIABLE .)) (A . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 2 .)(NIL . (DECL ADD1 (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (POSTFIXNAME: /') (BINDINGPOWER: 975)) . ((ADD1 . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 975) (POSTFIX& . /')) . NATNUM#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 3 .)(|NATNUM(0)| . (TRW (TM& . |NATNUM(0)|) NIL) . NIL . NIL . NIL . NIL . NATNUM . NIL . 4 .)(NIL . (DECL LESSP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: <) (BINDINGPOWER: 920)) . ((LESSP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . <)) . ORDERING#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . ORDERING . NIL . 1 .)(NIL . (DECL GREATERP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: >) (BINDINGPOWER: 920)) . ((GREATERP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . >)) . ORDERING#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . ORDERING . NIL . 2 .)(NIL . (DECL TIMES (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: *) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 935)) . ((TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . MULTIP#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . MULTIP . NIL . 1 .)(NIL . (DECL EPSILON (TYPE: (TY& . |((@ARB)⊗(@SETVAR))→TRUTHVAL|)) (INFIXNAME: ε) (BINDINGPOWER: 925)) . ((EPSILON . (|((@ARB)⊗(@SETVAR))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 925) (INFIX& . ε)) . SETS#3 . NIL . VARIABLE .)) SETVAR ARB) . NIL . NIL . NIL . SETS . NIL . 3 .)(|∀ARB1 OBJ1.ARB1εOBJ1≡OBJ1(ARB1)| . (DEFINE EPSILON (TM& . |∀ARB1 OBJ1.ARB1εOBJ1≡OBJ1(ARB1)|) NIL) . (ARB2 ARB1 ARB SETVAR (EPSILON . (|((@ARB)⊗(@SETVAR))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 925) (INFIX& . ε)) . SETS#4 . NIL . DEFINED .)) (OBJ1 . (|(?ARBITRARY)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#4 . NIL . VARIABLE .))) . NIL . (SETS#4) . NIL . SETS . NIL . 4 .)(|∀P P1 P2.P2∧(P∨P1)≡P2∧P∨P2∧P1| . (AXIOM (TM& . |∀P P1 P2.P2∧(P∨P1)≡P2∧P∨P2∧P1|)) . (P2 P1 P) . NIL . (NORMAL#2) . NIL . NORMAL . NIL . 2 .)(|∀P P1 P2.P2∧(P∨P1)≡P∧P2∨P1∧P2| . (AXIOM (TM& . |∀P P1 P2.P2∧(P∨P1)≡P∧P2∨P1∧P2|)) . (P2 P1 P) . NIL . (NORMAL#3) . NIL . NORMAL . NIL . 3 .)(|∀P P1 P2.(P∨P1⊃P2)≡(P⊃P2)∧(P1⊃P2)| . (AXIOM (TM& . |∀P P1 P2.(P∨P1⊃P2)≡(P⊃P2)∧(P1⊃P2)|)) . (P2 P1 P) . NIL . (NORMAL#4) . NIL . NORMAL . NIL . 4 .)(|∀P P1.¬(P∨P1)≡¬P∧¬P1| . (AXIOM (TM& . |∀P P1.¬(P∨P1)≡¬P∧¬P1|)) . (P2 P1 P) . NIL . (NORMAL#5) . NIL . NORMAL . NIL . 5 .)(|∀P P1.¬(P∧P1)≡¬P∨¬P1| . (AXIOM (TM& . |∀P P1.¬(P∧P1)≡¬P∨¬P1|)) . (P2 P1 P) . NIL . (NORMAL#6) . NIL . NORMAL . NIL . 6 .)(|∀P P1.P≡(P1⊃P)∧(¬P1⊃P)| . (AXIOM (TM& . |∀P P1.P≡(P1⊃P)∧(¬P1⊃P)|)) . (P2 P1 P) . NIL . (NORMAL#7) . NIL . NORMAL . NIL . 7 .)(|∀P P1 P2.(P1⊃P2)∧(IF P THEN P1 ELSE P2)⊃P2| . (AXIOM (TM& . |∀P P1 P2.(P1⊃P2)∧(IF P THEN P1 ELSE P2)⊃P2|)) . (P2 P1 P) . NIL . (NORMAL#8) . NIL . NORMAL . NIL . 8 .)(|∀P1 P2 P3 P4.(P2≡P4)∧(P1∨P2∨P3)⊃P1∨P4∨P3| . (AXIOM (TM& . |∀P1 P2 P3 P4.(P2≡P4)∧(P1∨P2∨P3)⊃P1∨P4∨P3|)) . (P2 P1 P (P4 . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 1000)) . NORMAL#9 . NIL . VARIABLE .)) (P3 . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 1000)) . NORMAL#9 . NIL . VARIABLE .))) . NIL . (NORMAL#9) . NIL . NORMAL . NIL . 9 .)(|∀P P1 P2.P∧P1⊃¬P2≡¬(P∧P1∧P2)| . (AXIOM (TM& . |∀P P1 P2.P∧P1⊃¬P2≡¬(P∧P1∧P2)|)) . (P2 P1 P) . NIL . (NORMAL#10) . NIL . NORMAL . NIL . 10 .)(|∀N.NATNUM(N')| . (AXIOM (TM& . |∀N.NATNUM(N')|)) . (M N K J I ADD1) . NIL . (NATNUM#5) . NIL . NATNUM . NIL . 5 .)(|∀N.¬N'=0| . (AXIOM (TM& . |∀N.¬N'=0|)) . (M N K J I ADD1) . NIL . (NATNUM#6) . NIL . NATNUM . NIL . 6 .)(|∀N M.N'=M'≡N=M| . (AXIOM (TM& . |∀N M.N'=M'≡N=M|)) . (M N K J I ADD1) . NIL . (NATNUM#7) . NIL . NATNUM . NIL . 7 .)(|∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))| . (AXIOM (TM& . |∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))|)) . (M N K J I SET C B A ADD1) . NIL . (NATNUM#8) . NIL . NATNUM . NIL . 8 .)(NIL . (DECL ALL (TYPE: (TY& . |(GROUND⊗(@SET))→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((ALL . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALL#1 . NIL . CONSTANT .)) SET) . NIL . NIL . NIL . ALL . NIL . 1 .)(NIL . (DECL SOME (TYPE: (TY& . |(GROUND⊗(@SET))→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((SOME . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALL#2 . NIL . CONSTANT .)) SET) . NIL . NIL . NIL . ALL . NIL . 2 .)(|∀N A.ALL(0,A)∧(ALL(N',A)≡A(N)∧ALL(N,A))| . (DEFAX ALL (TM& . |∀N A.ALL(0,A)∧(ALL(N',A)≡A(N)∧ALL(N,A))|)) . (M N K J I SET C B A ADD1 (ALL . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALL#3 . NIL . DEFINED .))) . NIL . (ALL#3) . NIL . ALL . NIL . 3 .)(|∀N A.¬SOME(0,A)∧(SOME(N',A)≡A(N)∨SOME(N,A))| . (DEFAX SOME (TM& . |∀N A.¬SOME(0,A)∧(SOME(N',A)≡A(N)∨SOME(N,A))|)) . (M N K J I SET C B A ADD1 (SOME . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALL#4 . NIL . DEFINED .))) . NIL . (ALL#4) . NIL . ALL . NIL . 4 .)(|∀SETVAR SETVAR1.(∀ARB.ARBεSETVAR≡ARBεSETVAR1)⊃SETVAR=SETVAR1| . (AXIOM (TM& . |∀SETVAR SETVAR1.(∀ARB.ARBεSETVAR≡ARBεSETVAR1)⊃SETVAR=SETVAR1|)) . (ARB2 ARB1 ARB SETVAR1 SETVAR EPSILON OBJ1) . NIL . (SETS#5) . NIL . SETS . NIL . 5 .)(NIL . (DECL FUNCTION (TYPE: (TY& . |((?ARBITRARY)*)→(?ARBITRARY)|)) (SYNTYPE: VARIABLE)) . ((FUNCTION . (|((?ARBITRARY)*)→(?ARBITRARY)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#6 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 6 .)(NIL . (DECL ZETA (TYPE: (TY& . |((?ARBITRARY)*)→TRUTHVAL|)) (SYNTYPE: VARIABLE)) . ((ZETA . (|((?ARBITRARY)*)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#7 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 7 .)(NIL . (DECL PARVAR (TYPE: (TY& . ?ARBITRARY)) (SYNTYPE: VARIABLE)) . ((PARVAR . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#8 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 8 .)(|∀M N.¬M=N⊃¬M'=N'| . (DERIVE (TM& . |∀M N.¬M=N⊃¬M'=N'|) ((LR& NATNUM#7)) NIL) . (M N K J I ADD1) . NIL . (NATNUM#5 NATNUM#6 NATNUM#7) . NIL . NATNUM . NIL . 9 .)(|∀N.¬N=N'| . (UE (UELST& (A . |λN.¬N=N'|)) (LN& . NATNUM#8) (USE (LR& NATNUM#7))) . (M N K J I SET C B A ADD1) . NIL . (NATNUM#8 NATNUM#5 NATNUM#6 NATNUM#7) . NIL . NATNUM . NIL . 10 .)(|∀N.¬N=0⊃(∃K.N=K')| . (UE (UELST& (A . |λN.¬N=0⊃(∃K.N=K')|)) (LN& . NATNUM#8) NIL) . (M N K J I SET C B A ADD1) . NIL . (NATNUM#8 NATNUM#5 NATNUM#6 NATNUM#7) . NIL . NATNUM . NIL . 11 .)(NIL . (DECL PLUS (INFIXNAME: +) (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 930)) . ((PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#12 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 12 .)(|∀N K.0+N=N∧K'+N=(K+N)'| . (DEFAX PLUS (TM& . |∀N K.0+N=N∧K'+N=(K+N)'|)) . (M N K J I ADD1 (PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#13 . NIL . DEFINED .))) . NIL . (NATNUM#13) . NIL . NATNUM . NIL . 13 .)(|(∀ARB1.(∃ARB2.ZETA(ARB1,ARB2,PARVAR)))⊃(∃FUNCTION.(∀ARB1.ZETA(ARB1,FUNCTION(ARB1,PARVAR),PARVAR)))| . (AXIOM (TM& . |(∀ARB1.(∃ARB2.ZETA(ARB1,ARB2,PARVAR)))⊃(∃FUNCTION.(∀ARB1.ZETA(ARB1,FUNCTION(ARB1,PARVAR),PARVAR)))|)) . (ARB2 ARB1 ARB FUNCTION ZETA PARVAR) . NIL . (SETS#9) . NIL . SETS . NIL . 9 .)(|∀N M.NATNUM(N+M)| . (AXIOM (TM& . |∀N M.NATNUM(N+M)|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#14) . NIL . NATNUM . NIL . 14 .)(|∀N M.(∃K.K=N+M∧(∀I J.I=M+N∧J=M+N⊃I=J))| . (AXIOM (TM& . |∀N M.(∃K.K=N+M∧(∀I J.I=M+N∧J=M+N⊃I=J))|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#15) . NIL . NATNUM . NIL . 15 .)(|∀N.N+0=N| . (AXIOM (TM& . |∀N.N+0=N|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#16) . NIL . NATNUM . NIL . 16 .)(|∀K N.K+N=N+K| . (AXIOM (TM& . |∀K N.K+N=N+K|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#17) . NIL . NATNUM . NIL . 17 .)(|∀N M.¬N=N+M'| . (AXIOM (TM& . |∀N M.¬N=N+M'|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#18) . NIL . NATNUM . NIL . 18 .)(|∀N K M.¬K=M⊃¬N+K=N+M| . (AXIOM (TM& . |∀N K M.¬K=M⊃¬N+K=N+M|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#19) . NIL . NATNUM . NIL . 19 .)(|∀N M.M=N∨(∃K.M=N+K')∨(∃K.N=M+K')| . (AXIOM (TM& . |∀N M.M=N∨(∃K.M=N+K')∨(∃K.N=M+K')|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#20) . NIL . NATNUM . NIL . 20 .)(|∀N M.M=N⊃¬(∃K.M=N+K')∧¬(∃K.N=M+K')| . (AXIOM (TM& . |∀N M.M=N⊃¬(∃K.M=N+K')∧¬(∃K.N=M+K')|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#21) . NIL . NATNUM . NIL . 21 .)(|∀N M.(∃K.M=N+K')⊃¬M=N∧¬(∃K.N=M+K')| . (AXIOM (TM& . |∀N M.(∃K.M=N+K')⊃¬M=N∧¬(∃K.N=M+K')|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#22) . NIL . NATNUM . NIL . 22 .)(|∀N M.(∃K.N=M+K')⊃¬M=N∧¬(∃K.M=N+K')| . (AXIOM (TM& . |∀N M.(∃K.N=M+K')⊃¬M=N∧¬(∃K.M=N+K')|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#23) . NIL . NATNUM . NIL . 23 .)(|∀N.1+N=N'∧N+1=N'| . (AXIOM (TM& . |∀N.1+N=N'∧N+1=N'|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#24) . NIL . NATNUM . NIL . 24 .)(|∀N K.N+K'=(N+K)'| . (AXIOM (TM& . |∀N K.N+K'=(N+K)'|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#25) . NIL . NATNUM . NIL . 25 .)(|∀N K M.K+M=K+N≡M=N| . (AXIOM (TM& . |∀N K M.K+M=K+N≡M=N|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#26) . NIL . NATNUM . NIL . 26 .)(|∀N K M.M+K=N+K≡M=N| . (AXIOM (TM& . |∀N K M.M+K=N+K≡M=N|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#27) . NIL . NATNUM . NIL . 27 .)(|∀N K.N+K=0≡N=0∧K=0| . (AXIOM (TM& . |∀N K.N+K=0≡N=0∧K=0|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#28) . NIL . NATNUM . NIL . 28 .)(|∀N M.N>M≡(∃K.N=M+K')| . (DEFAX GREATERP (TM& . |∀N M.N>M≡(∃K.N=M+K')|)) . (M N K J I ADD1 PLUS (GREATERP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . >)) . ORDERING#3 . NIL . DEFINED .))) . NIL . (ORDERING#3) . NIL . ORDERING . NIL . 3 .)(|∀N M.N<M≡(∃K.M=N+K')| . (DEFAX LESSP (TM& . |∀N M.N<M≡(∃K.M=N+K')|)) . (M N K J I ADD1 PLUS (LESSP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . <)) . ORDERING#4 . NIL . DEFINED .))) . NIL . (ORDERING#4) . NIL . ORDERING . NIL . 4 .)(|∀N K.0*N=0∧N'*K=N*K+K| . (DEFAX TIMES (TM& . |∀N K.0*N=0∧N'*K=N*K+K|)) . (M N K J I ADD1 PLUS (TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . MULTIP#2 . NIL . DEFINED .))) . NIL . (MULTIP#2) . NIL . MULTIP . NIL . 2 .)(|∀N M.M<N∨M=N∨M>N| . (AXIOM (TM& . |∀N M.M<N∨M=N∨M>N|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#5) . NIL . ORDERING . NIL . 5 .)(|∀N M.M=N⊃¬M<N∧¬M>N| . (AXIOM (TM& . |∀N M.M=N⊃¬M<N∧¬M>N|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#6) . NIL . ORDERING . NIL . 6 .)(|∀N M.M>N⊃¬M=N∧¬M<N| . (AXIOM (TM& . |∀N M.M>N⊃¬M=N∧¬M<N|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#7) . NIL . ORDERING . NIL . 7 .)(|∀N M.M<N⊃¬M=N∧¬M>N| . (AXIOM (TM& . |∀N M.M<N⊃¬M=N∧¬M>N|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#8) . NIL . ORDERING . NIL . 8 .)(|∀N M.M>N≡N<M| . (AXIOM (TM& . |∀N M.M>N≡N<M|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#9) . NIL . ORDERING . NIL . 9 .)(NIL . (DECL GRTEQP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: ≥) (BINDINGPOWER: 920)) . ((GRTEQP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≥)) . ORDERING#10 . NIL . CONSTANT .))) . NIL . NIL . NIL . ORDERING . NIL . 10 .)(NIL . (DECL LSSEQP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: ≤) (BINDINGPOWER: 920)) . ((LSSEQP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≤)) . ORDERING#11 . NIL . CONSTANT .))) . NIL . NIL . NIL . ORDERING . NIL . 11 .)(|∀N M.M≥N≡M>N∨M=N| . (DEFAX GRTEQP (TM& . |∀N M.M≥N≡M>N∨M=N|)) . (M N K J I ADD1 PLUS GREATERP (GRTEQP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≥)) . ORDERING#12 . NIL . DEFINED .))) . NIL . (ORDERING#12) . NIL . ORDERING . NIL . 12 .)(|∀N M.M≤N≡M<N∨M=N| . (DEFAX LSSEQP (TM& . |∀N M.M≤N≡M<N∨M=N|)) . (M N K J I ADD1 PLUS LESSP (LSSEQP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≤)) . ORDERING#13 . NIL . DEFINED .))) . NIL . (ORDERING#13) . NIL . ORDERING . NIL . 13 .)(|∀N M.NATNUM(N*M)| . (AXIOM (TM& . |∀N M.NATNUM(N*M)|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#3) . NIL . MULTIP . NIL . 3 .)(|∀N.N*0=0∧1*N=N∧N*1=N| . (AXIOM (TM& . |∀N.N*0=0∧1*N=N∧N*1=N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#4) . NIL . MULTIP . NIL . 4 .)(|∀K N.N*K'=N*K+N| . (AXIOM (TM& . |∀K N.N*K'=N*K+N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#5) . NIL . MULTIP . NIL . 5 .)(|∀N K M.¬K=0⊃K*M=K*N≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃K*M=K*N≡M=N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#6) . NIL . MULTIP . NIL . 6 .)(|∀N K M.¬K=0⊃M*K=N*K≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃M*K=N*K≡M=N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#7) . NIL . MULTIP . NIL . 7 .)(|∀N M.N*M=M*N| . (AXIOM (TM& . |∀N M.N*M=M*N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#8) . NIL . MULTIP . NIL . 8 .)(|∀N K.¬N=0⊃N*K=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃N*K=0≡K=0|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#9) . NIL . MULTIP . NIL . 9 .)(|∀N K.¬N=0⊃K*N=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃K*N=0≡K=0|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#10) . NIL . MULTIP . NIL . 10 .)(|∀A N.(∀M.M<N⊃A(M))≡ALL(N,A)| . (AXIOM (TM& . |∀A N.(∀M.M<N⊃A(M))≡ALL(N,A)|)) . (M N K J I SET C B A ADD1 PLUS LESSP ALL) . NIL . (ALL#5) . NIL . ALL . NIL . 5 .)(|∀A N.(∃M.M<N∧A(M))≡SOME(N,A)| . (AXIOM (TM& . |∀A N.(∃M.M<N∧A(M))≡SOME(N,A)|)) . (M N K J I SET C B A ADD1 PLUS LESSP SOME) . NIL . (ALL#6) . NIL . ALL . NIL . 6 .)(|∀N M.M≥N≡N≤M| . (AXIOM (TM& . |∀N M.M≥N≡N≤M|)) . (M N K J I ADD1 PLUS LESSP GREATERP GRTEQP LSSEQP) . NIL . (ORDERING#14) . NIL . ORDERING . NIL . 14 .)(|∀N M K.N<M∧M<K⊃N<K| . (AXIOM (TM& . |∀N M K.N<M∧M<K⊃N<K|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#15) . NIL . ORDERING . NIL . 15 .)(|∀N M K.K>M∧M>N⊃K>N| . (AXIOM (TM& . |∀N M K.K>M∧M>N⊃K>N|)) . (M N K J I ADD1 PLUS GREATERP) . NIL . (ORDERING#16) . NIL . ORDERING . NIL . 16 .)(|∀N M K.N≤M∧M<K⊃N<K| . (AXIOM (TM& . |∀N M K.N≤M∧M<K⊃N<K|)) . (M N K J I ADD1 PLUS LESSP LSSEQP) . NIL . (ORDERING#17) . NIL . ORDERING . NIL . 17 .)(|∀N M K.N<M∧M≤K⊃N<K| . (AXIOM (TM& . |∀N M K.N<M∧M≤K⊃N<K|)) . (M N K J I ADD1 PLUS LESSP LSSEQP) . NIL . (ORDERING#18) . NIL . ORDERING . NIL . 18 .)(|∀N M K.N≤M∧M≤K⊃N≤K| . (AXIOM (TM& . |∀N M K.N≤M∧M≤K⊃N≤K|)) . (M N K J I ADD1 PLUS LESSP LSSEQP) . NIL . (ORDERING#19) . NIL . ORDERING . NIL . 19 .)(|∀N M.N+M'>N| . (AXIOM (TM& . |∀N M.N+M'>N|)) . (M N K J I ADD1 PLUS GREATERP) . NIL . (ORDERING#20) . NIL . ORDERING . NIL . 20 .)(|∀N M.N'<M'≡N<M| . (AXIOM (TM& . |∀N M.N'<M'≡N<M|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#21) . NIL . ORDERING . NIL . 21 .)(|∀N M K.M+K>N+K≡M>N| . (AXIOM (TM& . |∀N M K.M+K>N+K≡M>N|)) . (M N K J I ADD1 PLUS GREATERP) . NIL . (ORDERING#22) . NIL . ORDERING . NIL . 22 .)(|∀N M K.M+K<N+K≡M<N| . (AXIOM (TM& . |∀N M K.M+K<N+K≡M<N|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#23) . NIL . ORDERING . NIL . 23 .)(|∀N M I J.N>M∧I>J⊃N+I>M+J| . (AXIOM (TM& . |∀N M I J.N>M∧I>J⊃N+I>M+J|)) . (M N K J I ADD1 PLUS GREATERP) . NIL . (ORDERING#24) . NIL . ORDERING . NIL . 24 .)(|∀N M I J.N≥M∧I>J⊃N+I>M+J| . (AXIOM (TM& . |∀N M I J.N≥M∧I>J⊃N+I>M+J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#25) . NIL . ORDERING . NIL . 25 .)(|∀N M I J.N>M∧I≥J⊃N+I>M+J| . (AXIOM (TM& . |∀N M I J.N>M∧I≥J⊃N+I>M+J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#26) . NIL . ORDERING . NIL . 26 .)(|∀N M I J.N≥M∧I≥J⊃N+I≥M+J| . (AXIOM (TM& . |∀N M I J.N≥M∧I≥J⊃N+I≥M+J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#27) . NIL . ORDERING . NIL . 27 .)(|∀N.N≥0| . (AXIOM (TM& . |∀N.N≥0|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#28) . NIL . ORDERING . NIL . 28 .)(|∀N.¬N<0| . (AXIOM (TM& . |∀N.¬N<0|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#29) . NIL . ORDERING . NIL . 29 .)(|∀N.¬N=0⊃0<N| . (AXIOM (TM& . |∀N.¬N=0⊃0<N|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#30) . NIL . ORDERING . NIL . 30 .)(|∀N.N'≥1| . (AXIOM (TM& . |∀N.N'≥1|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#31) . NIL . ORDERING . NIL . 31 .)(|∀N M.N>M⊃N≥M'| . (AXIOM (TM& . |∀N M.N>M⊃N≥M'|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#32) . NIL . ORDERING . NIL . 32 .)(|∀M N.M<N'⊃M≤N| . (AXIOM (TM& . |∀M N.M<N'⊃M≤N|)) . (M N K J I ADD1 PLUS LESSP LSSEQP) . NIL . (ORDERING#33) . NIL . ORDERING . NIL . 33 .)(|∀A.(∃M.A(M))⊃(∃N.A(N)∧(∀M.A(M)⊃N<M))| . (AXIOM (TM& . |∀A.(∃M.A(M))⊃(∃N.A(N)∧(∀M.A(M)⊃N<M))|)) . (M N K J I SET C B A ADD1 PLUS LESSP) . NIL . (ORDERING#34) . NIL . ORDERING . NIL . 34 .)(¬N=0∧¬M=0⊃¬N*M=0 . (DERIVE (TM& . ¬N=0∧¬M=0⊃¬N*M=0) ((LR& MULTIP#10)) NIL) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#10 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4) . NIL . MULTIP . NIL . 11 .)(|∀N K M.N*(K+M)=N*K+N*M| . (AXIOM (TM& . |∀N K M.N*(K+M)=N*K+N*M|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#12) . NIL . MULTIP . NIL . 12 .)(|∀N M K.(M+K)*N=M*N+K*N| . (AXIOM (TM& . |∀N M K.(M+K)*N=M*N+K*N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#13) . NIL . MULTIP . NIL . 13 .)(|∀N M K.N>M∧¬K=0⊃N*K>M*K| . (AXIOM (TM& . |∀N M K.N>M∧¬K=0⊃N*K>M*K|)) . (M N K J I ADD1 PLUS GREATERP TIMES) . NIL . (MULTIP#14) . NIL . MULTIP . NIL . 14 .)(|∀N M K.N<M∧¬K=0⊃N*K<M*K| . (AXIOM (TM& . |∀N M K.N<M∧¬K=0⊃N*K<M*K|)) . (M N K J I ADD1 PLUS LESSP TIMES) . NIL . (MULTIP#15) . NIL . MULTIP . NIL . 15 .)(|∀N M K.¬K=0∧M*K>N*K⊃M>N| . (AXIOM (TM& . |∀N M K.¬K=0∧M*K>N*K⊃M>N|)) . (M N K J I ADD1 PLUS GREATERP TIMES) . NIL . (MULTIP#16) . NIL . MULTIP . NIL . 16 .)(|∀N M K.¬K=0∧M*K=N*K⊃M=N| . (AXIOM (TM& . |∀N M K.¬K=0∧M*K=N*K⊃M=N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#17) . NIL . MULTIP . NIL . 17 .)(|∀N M K.¬K=0∧M*K<N*K⊃M<N| . (AXIOM (TM& . |∀N M K.¬K=0∧M*K<N*K⊃M<N|)) . (M N K J I ADD1 PLUS LESSP TIMES) . NIL . (MULTIP#18) . NIL . MULTIP . NIL . 18 .)(|∀N M I J.N>M∧I>J⊃N*I>M*J| . (AXIOM (TM& . |∀N M I J.N>M∧I>J⊃N*I>M*J|)) . (M N K J I ADD1 PLUS GREATERP TIMES) . NIL . (MULTIP#19) . NIL . MULTIP . NIL . 19 .)(|∀N M I J.¬M=0∧N≥M∧I>J⊃N*I>M*J| . (AXIOM (TM& . |∀N M I J.¬M=0∧N≥M∧I>J⊃N*I>M*J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP TIMES) . NIL . (MULTIP#20) . NIL . MULTIP . NIL . 20 .)(|∀N M I J.¬J=0∧N>M∧I≥J⊃N*I>M*J| . (AXIOM (TM& . |∀N M I J.¬J=0∧N>M∧I≥J⊃N*I>M*J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP TIMES) . NIL . (MULTIP#21) . NIL . MULTIP . NIL . 21 .)(|∀N M I J.N≥M∧I≥J⊃N*I≥M*J| . (AXIOM (TM& . |∀N M I J.N≥M∧I≥J⊃N*I≥M*J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP TIMES) . NIL . (MULTIP#22) . NIL . MULTIP . NIL . 22 .)